fix: cslib breakage from the mathlib rwaSuggestion linter - #50

Adapts `cslib` to two deprecations that the `downstream: update repo
cslib` merge
(ffe4553, the head of [run
34142798876](https://github.com/leanprover/downstream-lean4/actions/runs/34142798876))
brought in. Supersedes #53, which carried one of these two hunks and has
been made
`CONFLICTING` by that same merge.

### cslib (noncritical, `--wfail --iofail`)

The merge added

```lean
@[deprecated _root_.refl (since := "2026-09-07")]
theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a
```

in `Cslib/Foundations/Relation/Basic.lean`, and moved the existing
`@[deprecated Relation.ReflGen.stdSymm]` on `ReflGen.symmGen_symm` out
of
`Confluence.lean` into that same file. In both cases the replacement is
a
`Std.Refl`/`Std.Symm` *instance* rather than the lemma it replaces, so
since
lean4#14600 the deprecation linter reports a type mismatch:

```
warning: Cslib/Foundations/Relation/Basic.lean:60:2: The updated constant has a different type:
  ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α), r a a
instead of
  ∀ {α : Type u_1} {r : α → α → Prop} (a : α), MJoin r a a
```

`cslib` builds with `--wfail`, so both warnings are build failures. The
type
difference is intended — callers are meant to go through `_root_.refl`
and
`Std.Symm.symm`, which is also how the two lemmas are proved — so this
marks both
with `+typeChanged` (syntax from lean4#14570).

Because #53 fixed the `ReflGen.symmGen_symm` site at its old location in
`Confluence.lean`, it no longer applies and this PR replaces it. The
`MJoin.refl`
site is new in this run.

**Verified** on `nightly-2026-09-06`: `lake build --wfail --iofail`
(3212 jobs),
`lake test --wfail --iofail` (9094 jobs) and `lake lint` all pass for
`cslib`. The
build/test/lint runs also had #50's one-line `rwa` hunk applied in the
working copy,
because without it the build stops at
`Cslib.Computability.Languages.MyhillNerode`
before the later phases can run; the two changes are in different files
and
independent. With this commit alone, `Cslib.Foundations.Relation.Basic`
builds clean
and `MyhillNerode` is the only remaining logged failure.

### Not fixed here — already covered by open PRs

**`cslib`'s other failure**,
`Cslib.Computability.Languages.MyhillNerode` under
mathlib's `rwaSuggestion` linter, is #50, still `MERGEABLE` and still
applying to
the current sources. Both it and this PR are needed for `cslib` to
build.

**`reference-manual`**, the one critical repo in the red set, is #51,
still
`MERGEABLE`. Its only logged failure in this run is
`Manual.BuildTools.Lake.Config`
at exactly the six `Mismatched elaborated configuration output` sites
that #51 fills
in for `lean4#15015`'s new `precompileImports` / `precompileLibrary`
fields. Nothing
added here.

<!-- downstream-watch: unattended -->

Fixes the red [run
34341290563](https://github.com/leanprover/downstream-lean4/actions/runs/34341290563)
on `master` (`leanprover/lean4:nightly-2026-09-09`). One commit per
repo.

## reference-manual (critical)

Two failures, the second only visible once the first was fixed.

1. `Manual/BuildTools/Lake/CLI.lean:835: Mismatched 'lake --help'
output` — lean4#15005 re-sandboxed `lake challenge` with `bwrap` instead
of `landrun`, changing the `lake challenge --help` text that the
`lakeHelp challenge` block embeds verbatim. The block now carries the
current output, and the surrounding prose follows it: the `bubblewrap`
link and its unprivileged-user-namespaces/setuid requirement,
`COMPARATOR_BWRAP` in place of `COMPARATOR_LANDRUN`, and a rewritten
"Sandbox" section — the old one described Landlock's write/TCP bounds
and the `AF_UNIX` escape, neither of which applies to `bwrap`.

2. `Manual/BuildTools/Lake.lean:377: Docstring on `#guard_msgs` does not
match generated message` — the package facet that lean4#14990 adds is
called `defaultModules`; the manual had been adapted against that PR's
pr-release toolchain, where it was still `modules`. Renamed in the
`initPackageFacetConfigs` list. CI never reached this module: it imports
`Manual.BuildTools.Lake.CLI`, which failed first.

Verified: `lake build` passes in full. The repo defines no test or lint
driver (`lake check-test` / `lake check-lint` both fail), so those
phases are skipped, as in CI.

The new `defaultModules` facet still has no prose entry under "The
facets available for packages are", unlike its neighbours. Left for the
manual's authors — the block's `-- Always keep this in sync with the
description below` comment was already out of sync for `modules`.

## Not changed

* **cslib** and **repl** were red only downstream of mathlib4 (cslib
skipped, repl's `lake test` builds Mathlib). With the mathlib4 fix in
place, `cslib` passes `lake build --wfail --iofail`, `lake test --wfail
--iofail` and `lake lint`, and `repl` passes `lake build` and `lake
test`, all unmodified.
* PR #50 is now redundant — its `rwa` in
`Cslib/Computability/Languages/MyhillNerode.lean` is already in
`master`. It carries no unattended marker and has a comment on it, so it
has been left open.

#72)

Fixes the red `master` of [run
34667673197](https://github.com/leanprover/downstream-lean4/actions/runs/34667673197)
on `nightly-2026-09-11`.

### mathlib4

`downstream: update repo mathlib4` (afbdc87) split
`Mathlib/Data/Nat/MaxPowDiv.lean`
into `Mathlib/Data/Nat/PadicValNat.lean`. The old file carried a
downstream-added
`+typeChanged` marker on

```lean
@[deprecated pow_dvd_iff_le_padicValNat +typeChanged (since := "2026-03-15")]
alias ⟨_, maxPowDiv.le_of_dvd⟩ := pow_dvd_iff_le_padicValNat
```

and because the bot resolves merge conflicts in favour of upstream, the
marker went with
the old file. So lean4#14600's inexact-deprecation check fires again —
the alias is the
`mpr` of `pow_dvd_iff_le_padicValNat`, whose type is necessarily a
one-directional
implication rather than the iff it deprecates in favour of:

```
warning: Mathlib/Data/Nat/PadicValNat.lean:200:2: The updated constant has a different type:
  ∀ {p k n : ℕ}, p ≠ 1 → n ≠ 0 → (p ^ k ∣ n ↔ k ≤ padicValNat p n)
instead of
  ∀ {p k n : ℕ}, p ≠ 1 → n ≠ 0 → k ≤ padicValNat p n → p ^ k ∣ n
```

`mathlib4` builds with `--wfail`, so that one warning is the whole build
failure.
Re-added the marker, in the bare form the surrounding aliases in the
file use (the
target is inferred from the `alias`; `batteries`' own
`BatteriesTest/alias.lean` spells
this form out).

This deprecation is old (`since := "2026-03-15"`, present in
`v4.34.0-rc2`) and the
check is nightly-only, so the marker only ever lives downstream — an
upstream file
move silently reverts it, which is a new way for these markers to go
stale on top of
the two directions noted in #70.

### Verified

* `mathlib4` — `lake build Mathlib Archive Counterexamples Wanted
--wfail` (9060 jobs,
  no warnings), `lake test --iofail`, `lake lint`.
* `cslib` — CI only skipped it behind `mathlib4`; `lake build`, `lake
test` and
`lake lint` (all with `--wfail --iofail` as `repos.toml` asks) pass
unchanged, so it
needs no commit here. In particular the `rwaSuggestion` hunk that #50
still carries is
  no longer needed — `master`'s `cslib` is clean without it.

Nothing was left unfinished: `mathlib4` and `cslib` were the only two
repos red in the
run, and every other repo was green there.

<!-- downstream-watch: unattended -->